($\lambda$$T$,$L$,$i$,$j$,$z$. swap($L$;$i$;$j$)) $\in$ $T$:Type$\rightarrow$$L$:($T$ List)$\rightarrow\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$L$$\parallel$}}$$\rightarrow\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$L$$\parallel$}}$$\rightarrow\downarrow$True$\rightarrow$($T$ List)